/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓␈↓ 
'January 16, 1984 

␈↓ α∧␈↓α␈↓ ε⊃CS258 Handout 1

␈↓ α∧␈↓Here is the problem from the CS206 take-home.

␈↓ α∧␈↓4.␈α∂ ␈↓↓sublis[pattern,␈α∞alist]␈↓␈α∂is␈α∞the␈α∂result␈α∂of␈α∞making␈α∂the␈α∞substitutions␈α∂described␈α∞in␈α∂␈↓↓alist␈↓␈α∂in␈α∞␈↓↓pattern.␈↓
␈↓ α∧␈↓Thus

␈↓ α∧␈↓␈↓↓sublis␈↓[(PLUS␈α
X␈α
(TIMES␈α
X␈α
Y)␈α
A),␈α
((X.A)␈α
(Y.(PLUS␈α
X␈α
Y)))]␈α
=␈α
(PLUS␈α
A␈α
(TIMES␈α
A␈α∞(PLUS␈α
X
␈↓ α∧␈↓Y)) A)

␈↓ α∧␈↓␈↓↓match[pattern,expression,alist]␈↓␈α∪attempts␈α∪to␈α∪match␈α∪␈↓↓pattern␈↓␈α∪against␈α∪␈↓↓expression␈↓␈α∪to␈α∪produce␈α∪and
␈↓ α∧␈↓extension␈α⊂of␈α⊂␈↓↓alist␈↓␈α⊂such␈α⊃that␈α⊂substituting␈α⊂in␈α⊂the␈α⊂pattern␈α⊃according␈α⊂to␈α⊂the␈α⊂result␈α⊂will␈α⊃give␈α⊂back
␈↓ α∧␈↓␈↓↓expression␈↓.␈α If␈α
the␈αmatch␈α
is␈αunsuccessful,␈αthe␈α
value␈αis␈α
the␈αatom␈αNO.␈α
 It␈αis␈α
assumed␈αthat␈αa␈α
predicate
␈↓ α∧␈↓␈↓↓isvar␈↓␈α∞applicable␈α∞to␈α∂atoms␈α∞is␈α∞available␈α∞that␈α∂distinguishes␈α∞variables␈α∞from␈α∞other␈α∂atoms.␈α∞ Assuming
␈↓ α∧␈↓that ␈↓↓X␈↓ and ␈↓↓Y␈↓ are variables, we have

␈↓ α∧␈↓␈↓↓match␈↓[(PLUS X Y), (PLUS A (TIMES B C)),NIL] = ((X.A) (Y TIMES B C)),

␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓↓match␈↓[(PLUS X Y), (PLUS A (TIMES B C)),((X.B))] = NO.

␈↓ α∧␈↓a. Write recursive programs for ␈↓↓sublis␈↓ and ␈↓↓match.␈↓

␈↓ α∧␈↓b. Write accurately the sentence that expresses the fact that ␈↓↓sublis␈↓ and ␈↓↓match␈↓ are partial inverses.

␈↓ α∧␈↓c. Prove the sentence of part b.

␈↓ α∧␈↓Here␈α∞is␈α∞what␈α∞I␈α∞had␈α∞in␈α∞mind␈α∞for␈α∞the␈α∂solutions␈α∞of␈α∞parts␈α∞a␈α∞and␈α∞b.␈α∞ Part␈α∞c␈α∞is␈α∞accomplished␈α∂by␈α∞S-
␈↓ α∧␈↓expression␈α
induction␈α
on␈α
the␈α
structure␈α
of␈α␈↓↓pat␈↓.␈α
 Our␈α
problem␈α
is␈α
to␈α
set␈αthis␈α
up␈α
in␈α
EKL.␈α
 It␈α
is␈αin␈α
order
␈↓ α∧␈↓for students to work together on it.

␈↓ α∧␈↓sublis[pat,alist] ← if at pat
␈↓ α∧␈↓                    then [if isvar pat
␈↓ α∧␈↓                          then {assoc[pat,alist}[λz. if n z
␈↓ α∧␈↓                                                        then error[]
␈↓ α∧␈↓                                                        else d z]
␈↓ α∧␈↓                          else pat]
␈↓ α∧␈↓                    else sublis[a pat,alist].sublis[d pat,alist]

␈↓ α∧␈↓match[pat,exp,alist] ← if alist = NO
␈↓ α∧␈↓                       then NO
␈↓ α∧␈↓                       else if at pat
␈↓ α∧␈↓                       then [if isvar pat
␈↓ α∧␈↓                             then {assoc[pat,alist]}
␈↓ α∧␈↓                                  [λz.if n z
␈↓ α∧␈↓                                      then [pat.exp].alist
␈↓ α∧␈↓                                      else [if d z = exp
␈↓ α∧␈↓␈↓ u2


␈↓ α∧␈↓                                            then alist
␈↓ α∧␈↓                                            else NO]]
␈↓ α∧␈↓                              else [if pat = exp then alist else NO]]
␈↓ α∧␈↓                        else if at exp then NO
␈↓ α∧␈↓                        else match[d pat,d exp,match[a pat,a exp,alist]]

␈↓ α∧␈↓∀pat exp alist. match[pat,exp,alist] ≠ NO
␈↓ α∧␈↓                 ⊃ sublis[pat,match[pat,exp,alist]] = exp


␈↓ α∧␈↓␈↓ αTAttached␈αalso␈αis␈αIan␈αMason's␈αsolution␈αof␈αthe␈αproblem.␈α It␈αseemed␈αto␈αme␈αto␈αbe␈αthe␈αclearest␈αof
␈↓ α∧␈↓those submitted.